(*
 *  Francesco Cotto
 *
 *  Sperimentazione di PdP:
 *
 *    PiCalculus - Abstract Machine
 *
 *
 *
 *)



(*
 *  Lexical Analysis
 *)

(* Eccezione: caso Non Previsto o Non Possibile *)
exception NP;;

type const = Bool of bool | Int of int | Ch of string;;
type token = LxVar of string 
           | LxConst of const
           | LxOp of string
           | LxDef 
           | LxNew
           | LxIn 
           | LxOut | LxInput | LxRInput 
           | LxBracket of string
           | LxComma
           | LxPar
           | LxPrint
           | LxStop
           | LxIf | LxThen | LxElse
           | LxEnd ;;

   let c2s c = Char.escaped c ;;

   let isletter c = match c with
                      'a'..'z' -> true
                    | 'A'..'Z' -> true
                    | _ -> false

   let isint n = match n with 
                   '0'..'9' -> true
                 | _ -> false 

   let funit a = () ;;

   exception LexErr of string ;;

   let token2str t =
           match t with
              LxEnd -> "End"
              | LxVar(s) -> "LxVar "^s
              | LxConst(s) -> ( match s with
                                 Bool b -> "bool "^(string_of_bool b)
                                |Int  n -> "int "^(string_of_int n)
                                |Ch c -> "ch "^c
                              )
              | LxOp(s) -> "LxOp "^s
              | LxDef -> "def" 
              | LxNew -> "new"
              | LxIn -> "in"
              | LxOut -> "!"
              | LxInput -> "?"
              | LxRInput -> "?*"
              | LxBracket(s) -> "LxBracket "^s
              | LxComma -> ","
              | LxPar -> "|"
              | LxPrint -> "print"
              | LxIf -> "if"
              | LxThen -> "then"
              | LxElse -> "else"
              | LxStop -> "nil" ;;


(*
type source = String of string | File of string ;;

class InputStream(src : source) =
    object (s)

    val input = src

end;;
*)

class picscanner (str : string) =
   object (s)
   val str = str^"#"
   
   val mutable p = 0

   val mutable token = LxEnd

   method cur = token

   method nextchar = p <- p+1; str.[p]

   method curchar = str.[p]
(*
   method next =  token <- s#begintoken; 
                  print_string ("next="^(token2str s#cur)^"\n");
                  s#cur
*)                  
   method next =  token <- s#begintoken; s#cur


   method begintoken =  
         let cc = s#curchar
         in match cc with
         
          n when (isint n) 
             -> let rec rinteger acc =
                     if isint s#nextchar
                        then rinteger (acc^(c2s s#curchar))
                        else LxConst(Int (int_of_string acc))
                 in rinteger (c2s cc)

            
         | v when (isletter v)
             -> let rec rvar acc = funit s#nextchar;
                   if (isletter s#curchar) || (isint s#curchar)
                      then rvar (acc^(c2s s#curchar))
                      else ( match acc with
                               "true" | "false" -> LxConst(Bool (bool_of_string acc))
                             | "and" -> LxOp("and")
                             | "or" -> LxOp("or")
                             | "new" -> LxNew
                             | "in" -> LxIn
                             | "print" -> LxPrint
                             | "stop" -> LxStop
                             | "if" -> LxIf
                             | "then" -> LxThen
                             | "else" -> LxElse
                             | "def" -> LxDef
                             | v -> LxVar(v) )
                 in rvar (c2s cc)

         | '/' ->(
                  match s#nextchar with
                   '/' -> let rec skip c = if c != '\n'
                                            then skip s#nextchar
                                            else s#begintoken
                          in skip s#nextchar

                  |'*' -> let rec skip c = if (c='*') && (s#nextchar = '/')
                                              then (funit s#nextchar;s#begintoken)
                                              else skip s#nextchar
                          in skip s#nextchar

                  | _ -> LxOp("/")
                 )

         | '+' | '-' | '*' | '=' -> let cc = s#curchar in funit s#nextchar;LxOp(c2s cc)

         | '!' -> funit s#nextchar; LxOut

         | '?' -> if s#nextchar = '*'
                     then (funit s#nextchar; LxRInput)
                     else LxInput 

         | '|' -> funit s#nextchar; LxPar

         | '(' -> if s#nextchar = ')' 
                     then (funit s#nextchar; LxStop)
                     else LxBracket (c2s cc)

         | '[' | ']' | ')' -> funit s#nextchar; LxBracket (c2s cc)

         | ',' -> funit s#nextchar; LxComma

         | '.' -> funit s#nextchar; LxIn
         
     
         | '#' -> LxEnd 
          
         | ' ' | '\n' -> funit s#nextchar; s#begintoken

         | error -> raise (LexErr ("Carattere non valido:"^(c2s error)))
   end;;
   
(* Test scanner *)

let str = "(new c in (c?*[x,r]|r![x+1]))//c1 c2 c3\nprint/* */true/*c4*//**//******/false";;

let sc = (new picscanner(str))

let rec lt t sc = if t!=LxEnd 
              then lt sc#next sc
              else print_string "FINE" ;;

lt sc#next sc;;

(*
 * Syntactic Analysis
 *)

(* Type definition *)

type var = string;;

type exp =  Const of const
         | Var of var
         | Op of string * exp * exp ;;

type proc =  Zero 
          |  New of var * proc 
          |  In  of var * exp list * proc
          |  Out of var * exp list * proc
          |  Print of exp list * proc
          |  Inrec of var * exp list * proc
          |  Par of proc * proc
          |  Cond of exp * proc * proc ;;

(* aggiungere Cond of exp * proc * proc *)


exception SynErr of string ;;


let invertlist l =
        let rec aux li lo =
                match li with
                   [] -> lo
                |  i::l -> aux l (i::lo)
        in aux l [];;
                  
let makedef ln lp =
           let rec newlist ln lp =
           match ln with
             v::l -> New(v, newlist l lp)  
           | [] -> proclist lp
           and proclist lp = 
              match lp with
                p::[] -> p
              | p::l -> Par(p, proclist l)
              | _ -> raise (SynErr "Traduzione def: lista proc vuota!")
           in newlist ln lp;;


class picparser (scanner : picscanner) =
   object (s)
   val tok = scanner

   method pexp =
       match tok#cur with

           LxVar(v) 
                ->(
                    match tok#next with
                      LxOp(op) -> funit tok#next; Op(op, Var(v), s#pexp)
                    | LxBracket(")") -> Var(v)
                    | _ -> Var(v)
                   )
                
           | LxConst(c)  
                ->(
                    match tok#next with
                      LxOp(op) -> funit tok#next; Op(op, Const(c), s#pexp)
                    | LxBracket(")") -> Const(c)
                    | _ -> Const(c)
                   )
                
           | LxBracket("(") 
                ->( 
                   funit tok#next; 
                   let e = s#pexp
                   in match tok#cur with
                   LxBracket(")") -> funit tok#next; e
                      | _ -> raise (SynErr "Attesa ) in espressione")
                  )
          | error -> raise (SynErr ("Non atteso in espressione: "^(token2str error)))
      
                    
   method pvarlist = 
      let cc = tok#cur
      in match cc with
            LxBracket("]") -> []
          | _ -> let rec pvarlistaux vl =
                     let cc = tok#cur
                     in match cc, tok#next with
                           LxVar(v), LxComma -> funit tok#next; 
                                                pvarlistaux ((Var v)::vl)
                                
                        | LxVar(v), LxBracket("]") -> Var(v)::vl
             
                        | _ -> raise (SynErr "In param list atteso o LxVar, o LxVar]")
      
                  in pvarlistaux []
      
      
      
   method pexplist = 
       let cc = tok#cur
            in match cc with
                  LxBracket("]") -> []
                | _ -> let rec pexplistaux vl =
                           let e = s#pexp
                           in match tok#cur with
                                 LxComma -> funit tok#next; 
                                            pexplistaux (e::vl)
                                      
                              |  LxBracket("]") -> e::vl
                   
                              | _ -> raise (SynErr "In exp list atteso o , o ]")
            
                  in pexplistaux []
                  
                  
                  
   method paramlist io = match tok#cur with
                           LxBracket("[") 
                              -> ( funit tok#next;
                                   let pl = 
                                      match io with
				         LxOut -> s#pexplist
				       | LxInput|LxRInput -> s#pvarlist
                                       | _ -> raise NP 
				      in match tok#cur with
				            LxBracket("]") -> invertlist pl
				          | error -> raise (SynErr ("Errore in paramlist: atteso ] al posto di "^(token2str error)))
                                 )
                            
                         | error -> raise (SynErr ("Errore in paramlist: atteso [ al posto di "^(token2str error)))
                         
                          


   (* parsifica codice. se l'ultimo token e' EOF ok, altrimenti eccezione *)                      
   method beginparse = let p = s#parse
              in match tok#cur with
                   LxEnd -> p
                 | _ -> raise (SynErr "Atteso fine processo")
   
   
   (* scopo del metodo: non rendere necessarie le parentesi per iniziare un
    * processo, anche se compare in un if then else o in parallelo o in una
    * sequenza etc
    * In particolare, si occupa di associare a SX tanti processi in parallelo *)              
   method parse = let p1 = s#nextparse
                  in match tok#cur with
                       LxEnd | LxBracket(")") | LxElse | LxIn | LxOp("and") -> p1
                     | LxPar -> s#parparse p1
                     | _ -> raise (SynErr "Fine non corretta")
 
   (* per associare a sinistra i processi in parallelo usiamo un metodo con
    * accumulatore *)
   method parparse parprocacc = 
           let p2 = s#nextparse
           in match tok#cur with
               LxEnd | LxBracket(")") | LxElse | LxIn | LxOp("and") ->
                       Par(parprocacc,p2)
             | LxPar -> s#parparse (Par(parprocacc,p2))
             | _ -> raise (SynErr ("Non atteso: "^(token2str tok#cur)))
 

   method nextparse = funit tok#next; s#curparse

   (* riconosce un processo, e ricorsivamente eventuali processi in sequenza
    * Non cerca di riconoscere quello che sta dopo (cfr. parse) 
    * Eccezione: Il riconoscimento del new. new c in P|Q eq. (new c in P)|Q *)
   method curparse =
      match tok#cur with 
        LxStop -> 
           ( 
             match tok#next with
              _ -> Zero
           )

      | LxNew -> 
           ( 
              match tok#next,tok#next with
                LxVar(var), LxIn 
                   ->(let p = s#nextparse
                      in match tok#cur with
                           LxPar| LxBracket(")") | LxEnd -> New(var,p)
                         | _ -> raise (SynErr "Errore in new" )
                     )
              | _ -> raise (SynErr "Attesa var in new: new <var> in <proc>")
           ) 

      | LxVar(var) ->
           ( 
             let io = tok#next 
             in match io with
                  LxInput | LxOut | LxRInput -> 
                     ( funit tok#next;       
                       let pl = s#paramlist io
                       in
                                         (     
                                           match io, tok#next with
                                                LxInput,  nt  ->In(var,pl, s#psuffix nt)
                                              
  
                                              | LxRInput, nt  -> Inrec(var, pl, s#psuffix nt)
                                                                  
                                              | LxOut, nt -> Out(var, pl, s#psuffix nt)
                                                                 
                                              | _ ->raise (SynErr "atteso in")
                                          )
                                    
                     )        
                  | _ -> raise (SynErr "Era atteso ! o ? o ?*") 
           )                 
                           
      | LxPrint ->
           ( 
             let io = tok#next 
             in match io with
                   LxOut -> 
                     ( funit tok#next;       
                       let pl = s#paramlist io
                       in
                                         (     
                                           match io, tok#next with
                                              | LxOut, nt -> Print(pl, s#psuffix nt)
                                                                 
                                              | _ ->raise (SynErr "atteso in")
                                          )
                     )        
                  | _ -> raise (SynErr "Dopo print atteso out ! ") 
           ) 


      | LxIf -> 
           ( 
             funit tok#next; 
             let exp = s#pexp 
             in match tok#cur with
                  LxThen ->
                     (  
                       let pthen = s#parse
                       in match tok#cur with
                             LxElse -> 
                                 let pelse = s#parse
                                 in Cond(exp, pthen, pelse)
                          | _ -> raise (SynErr "Atteso else: if<exp>then<p>else<p>")
  
                     )
                | _ -> raise (SynErr "Atteso then: if<exp>then<p>else<p>")        
           )


      | LxDef ->
           (  
             let rec pairdef lv lp =
                    match tok#next with
                       LxVar(v) -> 
                          ( funit tok#next;
                            let vl = s#paramlist LxRInput
                            in      (
                                              match tok#next with
                                                LxOp("=")->
                                                   ( 
                                                     let p = s#parse
                                                     in let listvar = v::lv
                                                     in let listproc = (Inrec(v,vl,p))::lp
                                                     in match tok#cur with
                                                          LxOp("and") -> pairdef listvar listproc
                                                        | LxIn -> makedef
                                                        (invertlist listvar)
                                                        (invertlist (s#parse::listproc))
                                                        | error -> raise (SynErr ("Non atteso in def:"^(token2str error)))

                                                   )
                                              | _ -> raise (SynErr "Atteso = in def")
                                                
                                               
                                        )
                                       
                          )
                     | _ -> raise (SynErr "Attesa var in def")
                     
             in pairdef [] []
           )
           
      | LxBracket("(") ->  
           (
             let p = s#parse
             in match tok#cur with
                  LxBracket(")") -> funit tok#next; p
                | _ -> raise (SynErr "Attesa  )")
           )
            

      | LxEnd -> raise (SynErr "Trovata fine # non attesa") 

      | error -> raise (SynErr ("inizio di processo non valido:"^(token2str error)))


    method psuffix token = 
            match token with
              LxEnd -> Zero
            | LxIn -> s#nextparse
            | LxPar -> Zero
            | LxBracket(")") -> Zero
            | LxElse -> Zero
                        
            | _ -> raise (SynErr "atteso in")

end;;

(*
 * AbsSyn -> source
 *)

(* Sintassi astratta -> string pic *)


let rec exp_to_str e =
        match e with 
          Const(Bool b) -> string_of_bool b
        | Const(Int i) -> string_of_int i
        | Const(Ch c) -> c
        | Var v -> v
        | Op(ob, e1, e2) -> ("("^(exp_to_str e1)^" "^ob^" "^(exp_to_str e2)^")");;
        

let rec explist_to_str le = 
        match le with
          [] -> ""
        | e::l ->  let virgola = if l==[] then "" else "," 
                   in (exp_to_str e)^virgola^(explist_to_str l) ;;

let rec varlist_to_str lv = 
        match lv with
          [] -> ""
        | Var v::l -> let virgola = if l==[] then "" else "," 
                       in v^virgola^(varlist_to_str l) 
        | _ -> raise (SynErr "In varlist elemento non atteso");;

let rec as_to_str p = 
        match p with 
          Zero -> "()"
        | New(v, p) -> "new "^v^" in "^(as_to_str p)
        | In(v, lv, p) -> v^"?["^(varlist_to_str lv)^"]."^(as_to_str p) 
        | Out(v, le, p) ->  v^"!["^(explist_to_str le)^"]."^(as_to_str p)
        | Print(le, p) -> "print!["^(explist_to_str le)^"]."^(as_to_str p)
        | Inrec(v, lv, p) -> v^"?*["^(varlist_to_str lv)^"]."^(as_to_str p)
        | Par(p1, p2) -> "("^(as_to_str p1)^"|"^(as_to_str p2)^")" 
        | Cond(exp, t, e) 
             -> "(if "^(exp_to_str exp)^" then "^(as_to_str t)^" else "^(as_to_str e)^")";;


(*
 *  AST --> prolog tc
 *
Var ::= (a..z)+ . (0..9|a..z)*

Num ::= 0 | 1 | ...

Bool ::= true | false

Exp ::= Var | Num | Bool | Exp + Exp | Exp and Exp

Proc ::= stop | input(Var, Var*, Proc) | rec(Var, Var*, Proc)
      |  output(Var, Exp*, Proc) | par(Proc, Proc) | nu(Var, Proc)
      |  ite(Exp, Proc, Proc)

 *)

let rec ast2pl = function
	 Zero -> "stop" 
        |Par(p1,p2) -> "par("^(ast2pl p1)^","^(ast2pl p2)^")"
	|New(var,p) -> "nu("^var^","^(ast2pl p)^")"
        |In(var,varlist,p) -> "input("^var^",["^(varlist_to_str varlist)^"],"^(ast2pl p)^")" 
 	|Inrec(var,varlist,p) -> "rec("^var^",["^(varlist_to_str varlist)^"],"^(ast2pl p)^")"
	|Out(var,explist,p) -> "output("^var^",["^(explist_to_str explist)^"],"^(ast2pl p)^")"
	|Print(le,p) -> "output(print,["^(explist_to_str le)^"],"^(ast2pl p)^")" 
	|Cond(exp,t,e) -> "ite("^(exp_to_str exp)^","^(ast2pl t)^","^(ast2pl e)^")";;


(*

open Format;;

let rec ppas2cs ppf p=
        match p with
          Zero -> fprintf ppf "()"

        | New(v,p) -> 
              fprintf ppf "@[<v 3>new %s in @;@[" v;
              ppas2cs ppf p;
              fprintf ppf "@]@;@]"
        | In(v, lv, p) ->
              fprintf ppf "%s?[%s]." v (varlist_to_str lv);
              ppas2cs ppf p
        | Inrec(v, lv, p) ->
              fprintf ppf "%s?*[%s]." v (varlist_to_str lv);
              ppas2cs ppf p
        | Out(v, le, p) ->
              fprintf ppf "%s![%s]." v (explist_to_str le);
              ppas2cs ppf p
        | Print(le, p) -> 
              fprintf ppf "print![%s]." (explist_to_str le); 
              ppas2cs ppf p
        | Par(p1, p2) -> 
              fprintf ppf "(";
              ppas2cs ppf p1;
              fprintf ppf "|";
              ppas2cs ppf p2;
              fprintf ppf ")"
        | Cond(exp, t, e) ->
              fprintf ppf "(@[<v 2>if %s" (exp_to_str exp);
              fprintf ppf "@;then @[";
              ppas2cs ppf t;
              fprintf ppf "@]@;else @[";
              ppas2cs ppf e;
              fprintf ppf "@])@;@]";;
 

let pptest s =
        let sa = (new picparser(new picscanner(s)))#beginparse
        in ppas2cs std_formatter sa;;

 
(* test parser *)


let test s=
        print_string ("\n\n\n"^s^"\n");
        let sa = (new picparser(new picscanner(s)))#beginparse
        in print_string (as_to_str sa) ;;

let s1 = "(new c in c?[] | c?[])";;
let s2 = "a?[] | b?[] | new c in c?[]";;
let s3 = "a?[] | new c in c?[]";;
let s4 = "(a?[] | b?[] | c?[])" ;;
let s5 = "if false then a?[] | b?[] | c?[] else ()";;
let s6 = "(if (true) then (a?[] | b?[] | c?[]) else (()) )";;
test s1;;
test s2;;
test s3;;
test s4;;
test s5;;
test s6;;

pptest s6;;
*)

(* 
  
 p ::= () | stop
       ( <p> )
       <p> | <p>   // (p1 | p2) | p3
       new <var> in <p>
       <var>![<exp list>] 
       <var>?[<var list>]
       <var>?*[<var list>]
       <p> in <p>  |  <p> . <p>
       def <var>[<var list>]=<p> ( and <var>[<var list>]=<p> )* in <p>

*)

(* promemoria per def: 
	"in" e' usato sia nel costrutto def sia per mettere in seq. dei processi.
        Pertanto, o usare parentesi per isolare il processo o esplicitare "in ()"

test "def d1[da1]=(p1?[pa1]) and d2[da2]=(p2?[pa2]) in ()";;

*)

let test s = let ast = (new picparser(new picscanner(s)))#beginparse 
             in print_string ((ast2pl ast)^"\n"); ast ;;

